Mathematics in Lean

1.1. Getting Started

The goal of this book is to teach you to formalize mathematics using the Lean 4 interactive proof assistant. It assumes that you know some mathematics, but it does not require much. Although we will cover examples ranging from number theory to measure theory and analysis, we will focus on elementary aspects of those fields, in the hopes that if they are not familiar to you, you can pick them up as you go. We also don’t presuppose any background with formal methods. Formalization can be seen as a kind of computer programming: we will write mathematical definitions, theorems, and proofs in a regimented language, like a programming language, that Lean can understand. In return, Lean provides feedback and information, interprets expressions and guarantees that they are well-formed, and ultimately certifies the correctness of our proofs.

You can learn more about Lean from the Lean project page and the Lean community web pages. This tutorial is based on Lean’s large and ever-growing library, Mathlib. We also strongly recommend joining the Lean Zulip online chat group if you haven’t already. You’ll find a lively and welcoming community of Lean enthusiasts there, happy to answer questions and offer moral support.

Although you can read a pdf or html version of this book online, it is designed to be read interactively, running Lean from inside the VS Code editor. To get started:

1. Install Lean 4 and VS Code following these installation instructions.

2. Make sure you have git installed.

3. Follow these instructions to fetch the mathematics_in_lean repository and open it up in VS Code.

4. Each section in this book has an associated Lean file with examples and exercises. You can find them in the folder MIL, organized by chapter. We strongly recommend making a copy of that folder and experimenting and doing the exercises in that copy. This leaves the originals intact, and it also makes it easier to update the repository as it changes (see below). You can call the copy my_files or whatever you want and use it to create your own Lean files as well.

At that point, you can open the textbook in a side panel in VS Code as follows:

1. Type ctrl-shift-P (command-shift-P in macOS).

2. Type Lean 4: Docs: Show Documentation Resources in the bar that appears, and then press return. (You can press return to select it as soon as it is highlighted in the menu.)

3. In the window that opens, click on Mathematics in Lean.

Alternatively, you can run Lean and VS Code in the cloud, using Gitpod. You can find instructions as to how to do that on the Mathematics in Lean project page on Github. We still recommend working in a copy of the MIL folder, as described above.

This textbook and the associated repository are still a work in progress. You can update the repository by typing git pull followed by lake exe cache get inside the mathematics_in_lean folder. (This assumes that you have not changed the contents of the MIL folder, which is why we suggested making a copy.)

We intend for you to work on the exercises in the MIL folder while reading the textbook, which contains explanations, instructions, and hints. The text will often include examples, like this one:

#eval "Hello, World!"

You should be able to find the corresponding example in the associated Lean file. If you click on the line, VS Code will show you Lean’s feedback in the Lean Goal window, and if you hover your cursor over the #eval command VS Code will show you Lean’s response to this command in a pop-up window. You are encouraged to edit the file and try examples of your own.

This book moreover provides lots of challenging exercises for you to try. Don’t rush past these! Lean is about doing mathematics interactively, not just reading about it. Working through the exercises is central to the experience. You don’t have to do all of them; when you feel comfortable that you have mastered the relevant skills, feel free to move on. You can always compare your solutions to the ones in the solutions folder associated with each section.

1.2. Overview

Put simply, Lean is a tool for building complex expressions in a formal language known as dependent type theory.

Every expression has a type, and you can use the #check command to print it. Some expressions have types like ℕ or ℕ → ℕ. These are mathematical objects.

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

Some expressions have type Prop. These are mathematical statements.

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

Some expressions have a type, P, where P itself has type Prop. Such an expression is a proof of the proposition P.

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

If you manage to construct an expression of type FermatLastTheorem and Lean accepts it as a term of that type, you have done something very impressive. (Using sorry is cheating, and Lean knows it.) So now you know the game. All that is left to learn are the rules.

This book is complementary to a companion tutorial, Theorem Proving in Lean, which provides a more thorough introduction to the underlying logical framework and core syntax of Lean. Theorem Proving in Lean is for people who prefer to read a user manual cover to cover before using a new dishwasher. If you are the kind of person who prefers to hit the start button and figure out how to activate the potscrubber feature later, it makes more sense to start here and refer back to Theorem Proving in Lean as necessary.

Another thing that distinguishes Mathematics in Lean from Theorem Proving in Lean is that here we place a much greater emphasis on the use of tactics. Given that we are trying to build complex expressions, Lean offers two ways of going about it: we can write down the expressions themselves (that is, suitable text descriptions thereof), or we can provide Lean with instructions as to how to construct them. For example, the following expression represents a proof of the fact that if n is even then so is m * n:

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

The proof term can be compressed to a single line:

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

The following is, instead, a tactic-style proof of the same theorem, where lines starting with -- are comments, hence ignored by Lean:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
  rintro m n ⟨k, hk⟩
  -- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
  use m * k
  -- Substitute for `n`,
  rw [hk]
  -- and now it's obvious.
  ring

As you enter each line of such a proof in VS Code, Lean displays the proof state in a separate window, telling you what facts you have already established and what tasks remain to prove your theorem. You can replay the proof by stepping through the lines, since Lean will continue to show you the state of the proof at the point where the cursor is. In this example, you will then see that the first line of the proof introduces m and n (we could have renamed them at that point, if we wanted to), and also decomposes the hypothesis Even n to a k and the assumption that n = 2 * k. The second line, use m * k, declares that we are going to show that m * n is even by showing m * n = 2 * (m * k). The next line uses the rewrite tactic to replace n by 2 * k in the goal, and the ring tactic solves the resulting goal m * (2 * k) = 2 * (m * k).

The ability to build a proof in small steps with incremental feedback is extremely powerful. For that reason, tactic proofs are often easier and quicker to write than proof terms. There isn’t a sharp distinction between the two: tactic proofs can be inserted in proof terms, as we did with the phrase by rw [hk, mul_add] in the example above. We will also see that, conversely, it is often useful to insert a short proof term in the middle of a tactic proof. That said, in this book, our emphasis will be on the use of tactics.

In our example, the tactic proof can also be reduced to a one-liner:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

Here we have used tactics to carry out small proof steps. But they can also provide substantial automation, and justify longer calculations and bigger inferential steps. For example, we can invoke Lean’s simplifier with specific rules for simplifying statements about parity to prove our theorem automatically.

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

Another big difference between the two introductions is that Theorem Proving in Lean depends only on core Lean and its built-in tactics, whereas Mathematics in Lean is built on top of Lean’s powerful and ever-growing library, Mathlib. As a result, we can show you how to use some of the mathematical objects and theorems in the library, and some of the very useful tactics. This book is not meant to be used as an complete overview of the library; the community web pages contain extensive documentation. Rather, our goal is to introduce you to the style of thinking that underlies that formalization, and point out basic entry points so that you are comfortable browsing the library and finding things on your own.

Interactive theorem proving can be frustrating, and the learning curve is steep. But the Lean community is very welcoming to newcomers, and people are available on the Lean Zulip chat group round the clock to answer questions. We hope to see you there, and have no doubt that soon enough you, too, will be able to answer such questions and contribute to the development of Mathlib.

So here is your mission, should you choose to accept it: dive in, try the exercises, come to Zulip with questions, and have fun. But be forewarned: interactive theorem proving will challenge you to think about mathematics and mathematical reasoning in fundamentally new ways. Your life may never be the same.

Acknowledgments. We are grateful to Gabriel Ebner for setting up the infrastructure for running this tutorial in VS Code, and to Kim Morrison and Mario Carneiro for help porting it from Lean 4. We are also grateful for help and corrections from Takeshi Abe, Julian Berman, Alex Best, Thomas Browning, Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin, Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Mathieu Guay-Paquet, Marc Huisinga, Benjamin Jones, Julian Külshammer, Victor Liu, Jimmy Lu, Martin C. Martin, Giovanni Mascellani, John McDowell, Isaiah Mindich, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Pim Otte, Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Eric Wieser, and others. Our work has been partially supported by the Hoskinson Center for Formal Mathematics.

2.1. Calculating

We generally learn to carry out mathematical calculations without thinking of them as proofs. But when we justify each step in a calculation, as Lean requires us to do, the net result is a proof that the left-hand side of the calculation is equal to the right-hand side.

In Lean, stating a theorem is tantamount to stating a goal, namely, the goal of proving the theorem. Lean provides the rewriting tactic rw, to replace the left-hand side of an identity by the right-hand side in the goal. If a, b, and c are real numbers, mul_assoc a b c is the identity a * b * c = a * (b * c) and mul_comm a b is the identity a * b = b * a. Lean provides automation that generally eliminates the need to refer the facts like these explicitly, but they are useful for the purposes of illustration. In Lean, multiplication associates to the left, so the left-hand side of mul_assoc could also be written (a * b) * c. However, it is generally good style to be mindful of Lean’s notational conventions and leave out parentheses when Lean does as well.

Let’s try out rw.

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

The import lines at the beginning of the associated examples file import the theory of the real numbers from Mathlib, as well as useful automation. For the sake of brevity, we generally suppress information like this in the textbook.

You are welcome to make changes to see what happens. You can type the ℝ character as \R or \real in VS Code. The symbol doesn’t appear until you hit space or the tab key. If you hover over a symbol when reading a Lean file, VS Code will show you the syntax that can be used to enter it. If you are curious to see all available abbreviations, you can hit Ctrl-Shift-P and then type abbreviations to get access to the Lean 4: Show all abbreviations command. If your keyboard does not have an easily accessible backslash, you can change the leading character by changing the lean4.input.leader setting.

When a cursor is in the middle of a tactic proof, Lean reports on the current proof state in the Lean Infoview window. As you move your cursor past each step of the proof, you can see the state change. A typical proof state in Lean might look as follows:

1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4

The lines before the one that begins with ⊢ denote the context: they are the objects and assumptions currently at play. In this example, these include two objects, x and y, each a natural number. They also include three assumptions, labelled h₁, h₂, and h₃. In Lean, everything in a context is labelled with an identifier. You can type these subscripted labels as h\1, h\2, and h\3, but any legal identifiers would do: you can use h1, h2, h3 instead, or foo, bar, and baz. The last line represents the goal, that is, the fact to be proved. Sometimes people use target for the fact to be proved, and goal for the combination of the context and the target. In practice, the intended meaning is usually clear.

Try proving these identities, in each case replacing sorry by a tactic proof. With the rw tactic, you can use a left arrow (\l) to reverse an identity. For example, rw [← mul_assoc a b c] replaces a * (b * c) by a * b * c in the current goal. Note that the left-pointing arrow refers to going from right to left in the identity provided by mul_assoc, it has nothing to do with the left or right side of the goal.

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

You can also use identities like mul_assoc and mul_comm without arguments. In this case, the rewrite tactic tries to match the left-hand side with an expression in the goal, using the first pattern it finds.

example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

You can also provide partial information. For example, mul_comm a matches any pattern of the form a * ? and rewrites it to ? * a. Try doing the first of these examples without providing any arguments at all, and the second with only one argument.

example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

You can also use rw with facts from the local context.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h']
  rw [← mul_assoc]
  rw [h]
  rw [mul_assoc]

Try these, using the theorem sub_self for the second one:

example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
  sorry

example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := by
  sorry

Multiple rewrite commands can be carried out with a single command, by listing the relevant identities separated by commas inside the square brackets.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

You still see the incremental progress by placing the cursor after a comma in any list of rewrites.

Another trick is that we can declare variables once and for all outside an example or theorem. Lean then includes them automatically.

variable (a b c d e f : ℝ)

example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

Inspection of the tactic state at the beginning of the above proof reveals that Lean indeed included all variables. We can delimit the scope of the declaration by putting it in a section ... end block. Finally, recall from the introduction that Lean provides us with a command to determine the type of an expression:

section
variable (a b c : ℝ)

#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm

end

The #check command works for both objects and facts. In response to the command #check a, Lean reports that a has type ℝ. In response to the command #check mul_comm a b, Lean reports that mul_comm a b is a proof of the fact a * b = b * a. The command #check (a : ℝ) states our expectation that the type of a is ℝ, and Lean will raise an error if that is not the case. We will explain the output of the last three #check commands later, but in the meanwhile, you can take a look at them, and experiment with some #check commands of your own.

Let’s try some more examples. The theorem two_mul a says that 2 * a = a + a. The theorems add_mul and mul_add express the distributivity of multiplication over addition, and the theorem add_assoc expresses the associativity of addition. Use the #check command to see the precise statements.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  rw [mul_add, add_mul, add_mul]
  rw [← add_assoc, add_assoc (a * a)]
  rw [mul_comm b a, ← two_mul]

Whereas it is possible to figure out what it going on in this proof by stepping through it in the editor, it is hard to read on its own. Lean provides a more structured way of writing proofs like this using the calc keyword.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]

Notice that the proof does not begin with by: an expression that begins with calc is a proof term. A calc expression can also be used inside a tactic proof, but Lean interprets it as the instruction to use the resulting proof term to solve the goal. The calc syntax is finicky: the underscores and justification have to be in the format indicated above. Lean uses indentation to determine things like where a block of tactics or a calc block begins and ends; try changing the indentation in the proof above to see what happens.

One way to write a calc proof is to outline it first using the sorry tactic for justification, make sure Lean accepts the expression modulo these, and then justify the individual steps using tactics.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      sorry
    _ = a * a + (b * a + a * b) + b * b := by
      sorry
    _ = a * a + 2 * (a * b) + b * b := by
      sorry

Try proving the following identity using both a pure rw proof and a more structured calc proof:

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  sorry

The following exercise is a little more challenging. You can use the theorems listed underneath.

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  sorry

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

We can also perform rewriting in an assumption in the context. For example, rw [mul_comm a b] at hyp replaces a * b by b * a in the assumption hyp.

example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp'] at hyp
  rw [mul_comm d a] at hyp
  rw [← two_mul (a * d)] at hyp
  rw [← mul_assoc 2 a d] at hyp
  exact hyp

In the last step, the exact tactic can use hyp to solve the goal because at that point hyp matches the goal exactly.

We close this section by noting that Mathlib provides a useful bit of automation with a ring tactic, which is designed to prove identities in any commutative ring as long as they follow purely from the ring axioms, without using any local assumption.

example : c * b * a = b * (a * c) := by
  ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

The ring tactic is imported indirectly when we import Mathlib.Data.Real.Basic, but we will see in the next section that it can be used for calculations on structures other than the real numbers. It can be imported explicitly with the command import Mathlib.Tactic. We will see there are similar tactics for other common kind of algebraic structures.

There is a variation of rw called nth_rw that allows you to replace only particular instances of an expression in the goal. Possible matches are enumerated starting with 1, so in the following example, nth_rw 2 [h] replaces the second occurrence of a + b with c.

example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]
  rw [add_mul]

2.2. Proving Identities in Algebraic Structures

Mathematically, a ring consists of a collection of objects, $R$, operations $+$ $\times$, and constants $0$ and $1$, and an operation $x\mapsto -x$ such that:

• $R$ with $+$ is an abelian group, with $0$ as the additive identity and negation as inverse.

• Multiplication is associative with identity $1$, and multiplication distributes over addition.

In Lean, the collection of objects is represented as a type, R. The ring axioms are as follows:

variable (R : Type*) [Ring R]

#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

You will learn more about the square brackets in the first line later, but for the time being, suffice it to say that the declaration gives us a type, R, and a ring structure on R. Lean then allows us to use generic ring notation with elements of R, and to make use of a library of theorems about rings.

The names of some of the theorems should look familiar: they are exactly the ones we used to calculate with the real numbers in the last section. Lean is good not only for proving things about concrete mathematical structures like the natural numbers and the integers, but also for proving things about abstract structures, characterized axiomatically, like rings. Moreover, Lean supports generic reasoning about both abstract and concrete structures, and can be trained to recognize appropriate instances. So any theorem about rings can be applied to concrete rings like the integers, ℤ, the rational numbers, ℚ, and the complex numbers ℂ. It can also be applied to any instance of an abstract structure that extends rings, such as any ordered ring or any field.

Not all important properties of the real numbers hold in an arbitrary ring, however. For example, multiplication on the real numbers is commutative, but that does not hold in general. If you have taken a course in linear algebra, you will recognize that, for every $n$, the $n$ by $n$ matrices of real numbers form a ring in which commutativity usually fails. If we declare R to be a commutative ring, in fact, all the theorems in the last section continue to hold when we replace ℝ by R.

variable (R : Type*) [CommRing R]
variable (a b c d : R)

example : c * b * a = b * (a * c) := by ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

We leave it to you to check that all the other proofs go through unchanged. Notice that when a proof is short, like by ring or by linarith or by sorry, it is common (and permissible) to put it on the same line as the by. Good proof-writing style should strike a balance between concision and readability.

The goal of this section is to strengthen the skills you have developed in the last section and apply them to reasoning axiomatically about rings. We will start with the axioms listed above, and use them to derive other facts. Most of the facts we prove are already in Mathlib. We will give the versions we prove the same names to help you learn the contents of the library as well as the naming conventions.

Lean provides an organizational mechanism similar to those used in programming languages: when a definition or theorem foo is introduced in a namespace bar, its full name is bar.foo. The command open bar later opens the namespace, which allows us to use the shorter name foo. To avoid errors due to name clashes, in the next example we put our versions of the library theorems in a new namespace called MyRing.

The next example shows that we do not need add_zero or add_right_neg as ring axioms, because they follow from the other axioms.

namespace MyRing
variable {R : Type*} [Ring R]

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]

theorem add_right_neg (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]

#check MyRing.add_zero
#check add_zero

end MyRing

The net effect is that we can temporarily reprove a theorem in the library, and then go on using the library version after that. But don’t cheat! In the exercises that follow, take care to use only the general facts about rings that we have proved earlier in this section.

(If you are paying careful attention, you may have noticed that we changed the round brackets in (R : Type*) for curly brackets in {R : Type*}. This declares R to be an implicit argument. We will explain what this means in a moment, but don’t worry about it in the meanwhile.)

Here is a useful theorem:

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc, neg_add_cancel, zero_add]

Prove the companion version:

theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
  sorry

Use these to prove the following:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  sorry

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
  sorry

With enough planning, you can do each of them with three rewrites.

We will now explain the use of the curly braces. Imagine you are in a situation where you have a, b, and c in your context, as well as a hypothesis h : a + b = a + c, and you would like to draw the conclusion b = c. In Lean, you can apply a theorem to hypotheses and facts just the same way that you can apply them to objects, so you might think that add_left_cancel a b c h is a proof of the fact b = c. But notice that explicitly writing a, b, and c is redundant, because the hypothesis h makes it clear that those are the objects we have in mind. In this case, typing a few extra characters is not onerous, but if we wanted to apply add_left_cancel to more complicated expressions, writing them would be tedious. In cases like these, Lean allows us to mark arguments as implicit, meaning that they are supposed to be left out and inferred by other means, such as later arguments and hypotheses. The curly brackets in {a b c : R} do exactly that. So, given the statement of the theorem above, the correct expression is simply add_left_cancel h.

To illustrate, let us show that a * 0 = 0 follows from the ring axioms.

theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]

We have used a new trick! If you step through the proof, you can see what is going on. The have tactic introduces a new goal, a * 0 + a * 0 = a * 0 + 0, with the same context as the original goal. The fact that the next line is indented indicates that Lean is expecting a block of tactics that serves to prove this new goal. The indentation therefore promotes a modular style of proof: the indented subproof establishes the goal that was introduced by the have. After that, we are back to proving the original goal, except a new hypothesis h has been added: having proved it, we are now free to use it. At this point, the goal is exactly the result of add_left_cancel h.

We could equally well have closed the proof with apply add_left_cancel h or exact add_left_cancel h. The exact tactic takes as argument a proof term which completely proves the current goal, without creating any new goal. The apply tactic is a variant whose argument is not necessarily a complete proof. The missing pieces are either inferred automatically by Lean or become new goals to prove. While the exact tactic is technically redundant since it is strictly less powerful than apply, it makes proof scripts slightly clearer to human readers and easier to maintain when the library evolves.

Remember that multiplication is not assumed to be commutative, so the following theorem also requires some work.

theorem zero_mul (a : R) : 0 * a = 0 := by
  sorry

By now, you should also be able replace each sorry in the next exercise with a proof, still using only facts about rings that we have established in this section.

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  sorry

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  sorry

theorem neg_zero : (-0 : R) = 0 := by
  apply neg_eq_of_add_eq_zero
  rw [add_zero]

theorem neg_neg (a : R) : - -a = a := by
  sorry

We had to use the annotation (-0 : R) instead of 0 in the third theorem because without specifying R it is impossible for Lean to infer which 0 we have in mind, and by default it would be interpreted as a natural number.

In Lean, subtraction in a ring is provably equal to addition of the additive inverse.

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b

On the real numbers, it is defined that way:

example (a b : ℝ) : a - b = a + -b :=
  rfl

example (a b : ℝ) : a - b = a + -b := by
  rfl

The proof term rfl is short for “reflexivity”. Presenting it as a proof of a - b = a + -b forces Lean to unfold the definition and recognize both sides as being the same. The rfl tactic does the same. This is an instance of what is known as a definitional equality in Lean’s underlying logic. This means that not only can one rewrite with sub_eq_add_neg to replace a - b = a + -b, but in some contexts, when dealing with the real numbers, you can use the two sides of the equation interchangeably. For example, you now have enough information to prove the theorem self_sub from the last section:

theorem self_sub (a : R) : a - a = 0 := by
  sorry

Show that you can prove this using rw, but if you replace the arbitrary ring R by the real numbers, you can also prove it using either apply or exact.

Lean knows that 1 + 1 = 2 holds in any ring. With a bit of effort, you can use that to prove the theorem two_mul from the last section:

theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
  norm_num

theorem two_mul (a : R) : 2 * a = a + a := by
  sorry

We close this section by noting that some of the facts about addition and negation that we established above do not need the full strength of the ring axioms, or even commutativity of addition. The weaker notion of a group can be axiomatized as follows:

variable (A : Type*) [AddGroup A]

#check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c))
#check (zero_add : ∀ a : A, 0 + a = a)
#check (neg_add_cancel : ∀ a : A, -a + a = 0)

It is conventional to use additive notation when the group operation is commutative, and multiplicative notation otherwise. So Lean defines a multiplicative version as well as the additive version (and also their abelian variants, AddCommGroup and CommGroup).

variable {G : Type*} [Group G]

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)

If you are feeling cocky, try proving the following facts about groups, using only these axioms. You will need to prove a number of helper lemmas along the way. The proofs we have carried out in this section provide some hints.

theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
  sorry

theorem mul_one (a : G) : a * 1 = a := by
  sorry

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  sorry

Explicitly invoking those lemmas is tedious, so Mathlib provides tactics similar to ring in order to cover most uses: group is for non-commutative multiplicative groups, abel for abelian additive groups, and noncomm_ring for non-commutative rings. It may seem odd that the algebraic structures are called Ring and CommRing while the tactics are named noncomm_ring and ring. This is partly for historical reasons, but also for the convenience of using a shorter name for the tactic that deals with commutative rings, since it is used more often.

2.3. Using Theorems and Lemmas

Rewriting is great for proving equations, but what about other sorts of theorems? For example, how can we prove an inequality, like the fact that $a+e^b\le a+e^c$ holds whenever $b\le c$? We have already seen that theorems can be applied to arguments and hypotheses, and that the apply and exact tactics can be used to solve goals. In this section, we will make good use of these tools.

Consider the library theorems le_refl and le_trans:

#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)

As we explain in more detail in Section 3.1, the implicit parentheses in the statement of le_trans associate to the right, so it should be interpreted as a ≤ b → (b ≤ c → a ≤ c). The library designers have set the arguments a, b and c to le_trans implicit, so that Lean will not let you provide them explicitly (unless you really insist, as we will discuss later). Rather, it expects to infer them from the context in which they are used. For example, when hypotheses h : a ≤ b and h' : b ≤ c are in the context, all the following work:

variable (h : a ≤ b) (h' : b ≤ c)

#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)

The apply tactic takes a proof of a general statement or implication, tries to match the conclusion with the current goal, and leaves the hypotheses, if any, as new goals. If the given proof matches the goal exactly (modulo definitional equality), you can use the exact tactic instead of apply. So, all of these work:

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x

In the first example, applying le_trans creates two goals, and we use the dots to indicate where the proof of each begins. The dots are optional, but they serve to focus the goal: within the block introduced by the dot, only one goal is visible, and it must be completed before the end of the block. Here we end the first block by starting a new one with another dot. We could just as well have decreased the indentation. In the fourth example and in the last example, we avoid going into tactic mode entirely: le_trans h₀ h₁ and le_refl x are the proof terms we need.

Here are a few more library theorems:

#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

Use them together with apply and exact to prove the following:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  sorry

In fact, Lean has a tactic that does this sort of thing automatically:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith

The linarith tactic is designed to handle linear arithmetic.

example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
  linarith

In addition to equations and inequalities in the context, linarith will use additional inequalities that you pass as arguments. In the next example, exp_le_exp.mpr h' is a proof of exp b ≤ exp c, as we will explain in a moment. Notice that, in Lean, we write f x to denote the application of a function f to the argument x, exactly the same way we write h x to denote the result of applying a fact or theorem h to the argument x. Parentheses are only needed for compound arguments, as in f (x + y). Without the parentheses, f x + y would be parsed as (f x) + y.

example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
  linarith [exp_le_exp.mpr h']

Here are some more theorems in the library that can be used to establish inequalities on the real numbers.

#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_left : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_right : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_left

Some of the theorems, exp_le_exp, exp_lt_exp use a bi-implication, which represents the phrase “if and only if.” (You can type it in VS Code with \lr of \iff). We will discuss this connective in greater detail in the next chapter. Such a theorem can be used with rw to rewrite a goal to an equivalent one:

example (h : a ≤ b) : exp a ≤ exp b := by
  rw [exp_le_exp]
  exact h

In this section, however, we will use the fact that if h : A ↔ B is such an equivalence, then h.mp establishes the forward direction, A → B, and h.mpr establishes the reverse direction, B → A. Here, mp stands for “modus ponens” and mpr stands for “modus ponens reverse.” You can also use h.1 and h.2 for h.mp and h.mpr, respectively, if you prefer. Thus the following proof works:

example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

The first line, apply add_lt_add_of_lt_of_le, creates two goals, and once again we use a dot to separate the proof of the first from the proof of the second.

Try the following examples on your own. The example in the middle shows you that the norm_num tactic can be used to solve concrete numeric goals.

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry

example : (0 : ℝ) < 1 := by norm_num

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  have h₀ : 0 < 1 + exp a := by sorry
  apply log_le_log h₀
  sorry

From these examples, it should be clear that being able to find the library theorems you need constitutes an important part of formalization. There are a number of strategies you can use:

• You can browse Mathlib in its GitHub repository.

• You can use the API documentation on the Mathlib web pages.

• You can rely on Mathlib naming conventions and Ctrl-space completion in the editor to guess a theorem name (or Cmd-space on a Mac keyboard). In Lean, a theorem named A_of_B_of_C establishes something of the form A from hypotheses of the form B and C, where A, B, and C approximate the way we might read the goals out loud. So a theorem establishing something like x + y ≤ ... will probably start with add_le. Typing add_le and hitting Ctrl-space will give you some helpful choices. Note that hitting Ctrl-space twice displays more information about the available completions.

• If you right-click on an existing theorem name in VS Code, the editor will show a menu with the option to jump to the file where the theorem is defined, and you can find similar theorems nearby.

• You can use the apply? tactic, which tries to find the relevant theorem in the library.

example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

To try out apply? in this example, delete the exact command and uncomment the previous line. Using these tricks, see if you can find what you need to do the next example:

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  sorry

Using the same tricks, confirm that linarith instead of apply? can also finish the job.

Here is another example of an inequality:

example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
  calc
    a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg

  calc
    2 * a * b = 2 * a * b + 0 := by ring
    _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) := add_le_add (le_refl _) h
    _ = a ^ 2 + b ^ 2 := by ring

Mathlib tends to put spaces around binary operations like * and ^, but in this example, the more compressed format increases readability. There are a number of things worth noticing. First, an expression s ≥ t is definitionally equivalent to t ≤ s. In principle, this means one should be able to use them interchangeably. But some of Lean’s automation does not recognize the equivalence, so Mathlib tends to favor ≤ over ≥. Second, we have used the ring tactic extensively. It is a real timesaver! Finally, notice that in the second line of the second calc proof, instead of writing by exact add_le_add (le_refl _) h, we can simply write the proof term add_le_add (le_refl _) h.

In fact, the only cleverness in the proof above is figuring out the hypothesis h. Once we have it, the second calculation involves only linear arithmetic, and linarith can handle it:

example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
  calc
    a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg
  linarith

How nice! We challenge you to use these ideas to prove the following theorem. You can use the theorem abs_le'.mpr. You will also need the constructor tactic to split a conjunction to two goals; see Section 3.4.

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
  sorry

#check abs_le'.mpr

If you managed to solve this, congratulations! You are well on your way to becoming a master formalizer.

2.4. More examples using apply and rw

The min function on the real numbers is uniquely characterized by the following three facts:

#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)

Can you guess the names of the theorems that characterize max in a similar way?

Notice that we have to apply min to a pair of arguments a and b by writing min a b rather than min (a, b). Formally, min is a function of type ℝ → ℝ → ℝ. When we write a type like this with multiple arrows, the convention is that the implicit parentheses associate to the right, so the type is interpreted as ℝ → (ℝ → ℝ). The net effect is that if a and b have type ℝ then min a has type ℝ → ℝ and min a b has type ℝ, so min acts like a function of two arguments, as we expect. Handling multiple arguments in this way is known as currying, after the logician Haskell Curry.

The order of operations in Lean can also take some getting used to. Function application binds tighter than infix operations, so the expression min a b + c is interpreted as (min a b) + c. With time, these conventions will become second nature.

Using the theorem le_antisymm, we can show that two real numbers are equal if each is less than or equal to the other. Using this and the facts above, we can show that min is commutative:

example : min a b = min b a := by
  apply le_antisymm
  · show min a b ≤ min b a
    apply le_min
    · apply min_le_right
    apply min_le_left
  · show min b a ≤ min a b
    apply le_min
    · apply min_le_right
    apply min_le_left

Here we have used dots to separate proofs of different goals. Our usage is inconsistent: at the outer level, we use dots and indentation for both goals, whereas for the nested proofs, we use dots only until a single goal remains. Both conventions are reasonable and useful. We also use the show tactic to structure the proof and indicate what is being proved in each block. The proof still works without the show commands, but using them makes the proof easier to read and maintain.

It may bother you that the proof is repetitive. To foreshadow skills you will learn later on, we note that one way to avoid the repetition is to state a local lemma and then use it:

example : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    apply min_le_right
    apply min_le_left
  apply le_antisymm
  apply h
  apply h

We will say more about the universal quantifier in Section 3.1, but suffice it to say here that the hypothesis h says that the desired inequality holds for any x and y, and the intro tactic introduces an arbitrary x and y to establish the conclusion. The first apply after le_antisymm implicitly uses h a b, whereas the second one uses h b a.

Another solution is to use the repeat tactic, which applies a tactic (or a block) as many times as it can.

example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left

We encourage you to prove the following as exercises. You can use either of the tricks just described to shorten the first.